/*
 * Clause.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef CLAUSE_HPP_
#define CLAUSE_HPP_

#include <string>
#include <iostream>
#include <sstream>

#include <boost/unordered_set.hpp>

#include "bfr/Literal.hpp"

namespace bfr {

/**
 * Class representing a clause in a DNF / CNF.
 *
 * A clause is just a set of Literal objects.
 *
 * It actually stores the Literals in a
 * <a href="http://www.boost.org/doc/libs/1_49_0/doc/html/boost/unordered_set.html">
 * boost::unordered_set</a>.
 */
class Clause {

    private:
        /**
         * Type of the set that holds the Literals.
         */
        typedef boost::unordered_set<Literal, literal_hash_struct,
                literal_equals_struct> hash_clauses_t;

    public:
        /**
         * Iterator over all Literal objects in the Clause.
         */
        // TODO: make also pointers const?
        typedef hash_clauses_t::const_iterator const_iterator;

        Clause();

        /**
         * Create a Clause given an initial size.
         *
         * The initialSize is used to create a hash map
         * that is big enough to hold the number of elements
         * without expensive rehashing.
         *
         * Of course you can add more elements than initial size,
         * but then maybe some rehashing will bee done.
         *
         * Actually we create a hash set of size
         * \f$2 \cdot initialSize\f$.
         * I think this is too much... We can run some tests maybe.
         *
         * @param initialSize The size at the beginning.
         */
        explicit Clause(size_t initialSize);

        /**
         * Destructor.
         *
         * This will also destroy all Literals in the Clause.
         */
        ~Clause();

        /**
         * A struct that can be used to calculate the hash value.
         */
        struct clause_hash_struct : public std::unary_function<const Clause*,
                                                               size_t> {
            public:
                size_t operator()(const Clause *clause) const {
                    return clause->hashValue();
                }
        };

        /**
         * A struct that can be used to compare clauses.
         */
        struct clause_equals_struct :
            public std::binary_function<const Clause*,
                                        const Clause*,
                                        bool> {
            public:
                bool operator()(const Clause* c1,
                                 const Clause* c2) const {
                    return c1->operator==(*c2);
                }

        };

        /**
         * Add a Literal to the Clause.
         *
         * A copy of the literal is created.
         *
         * @param literal Literal to add.
         *
         * @return Returns <code>true</code> if the insertion took place
         * (i. e. an equivalent Literal has not been added before).
         */
        bool add(const Literal &literal);

        /**
         * Check whether the Clause contains a specific Literal.
         *
         * @param literal The Literal to check.
         *
         * @return <code>true</code> if the Clause contains the Literal.
         */
        bool contains(const Literal &literal) const;

        /**
         * Return the size of this Clause (number of Literals in it).
         *
         * @return Number of Literals in the Clause.
         */
        size_t size() const;

        /**
         * Return an iterator to the beginning.
         *
         * @return An iterator to the beginning.
         */
        const_iterator begin() const;

        /**
         * Return an iterator to the end.
         *
         * @return An iterator to the end.
         */
        const_iterator end() const;

         /**
          * Return a string representation of the Clause.
          *
          * @return Human readable string representation of the Clause.
          */
         std::string asString() const;

         /**
          * Calculate the hash value of this clause.
          *
          * The runtime is currently in \f$\mathcal{O}(n)\f$ where
          * \f$n\f$ is the number of literals in the clause.
          *
          * @return Hash value.
          */
         size_t hashValue() const;

         /**
          * Compare two Clauses.
          *
          * Two clauses are equal if they contain exactly the
          * same literals.
          *
          * Runtime is \f$\mathcal{O}(n)\f$ where \f$n\f$ is the number
          * of literals in the clauses (if they have a different
          * number of Literals it has constant runtime).
          *
          * So this operator does <b>not</b> check for semantic
          * equivalence.
          *
          * @return <code>true</code> if the other clause is equal
          * to this one.
          *
          */
         bool operator ==(const Clause &other) const;

         /**
          * Return the max. literal id over all Literals.
          *
          * To be more precisely this method returns the biggest
          * variable id of all literals in the clause.
          *
          * The method returns 0 even if the clause is empty.
          *
          * @return Biggest variable id of all Literals.
          */
         size_t getMaxLiteralId() const;

         /**
          * Evaluate the truth value of this Clause interpreted as a
          * conjunction.
          *
          * @param v The valuation function that must be defined for all
          * literal ids that occur in this clause.
          *
          * This method returns <code>true</code> if all literals in this
          * clause are consistent with the assignment v.
          *
          * I.e. the method checks that if literal with id <i>i</i>
          * occurs positive in the clause valuation for \f$x_i\f$ position
          * is true, if the literal is negative it checks if the valuation
          * for \f$x_i\f$ is false.
          *
          * If it finds one literal for which the above condition does not
          * hold it returns <code>false</code>.
          *
          * Runtime is in \f$O(n)\f$
          *
          * @return <code>true</code> If the conjunction defined by this clause
          * is true given the assignment defined by the mapping v.
          */
         template<class T>
         bool evaluateConjunction(const T &v) const {
                 const_iterator e = end();
                 for (const_iterator it = begin(); it != e; it++) {
                     const Literal &l = *it;
                     if (l.getPolarity()) {
                         if (!v[l.getId()])
                             return false;
                     } else {
                         if (v[l.getId()])
                             return false;
                     }
                 }
                 return true;
             }

         /**
          * Evaluate the truth value of this Clause interpreted as a
          * disjunction.
          *
          * @param v The valuation function that must be defined for all
          * literal ids that occur in this clause.
          *
          * This method returns <code>true</code> if one of the literals in
          * this clause is consistent with the assignment v.
          *
          * I.e. the method checks that if literal with id <i>i</i>
          * occurs positive in the clause the assignment for \f$x_i\f$
          * is true, if the literal is negative it checks if assignment for
          * \f$x_i\f$ is false.
          *
          * If it finds one literal for which the above condition holds
          * it returns <code>true</code>.
          *
          * @return <code>true</code> If the disjunction defined by this clause
          * is true given the assignment defined by the mapping v.
          */
         template<class T>
         bool evaluateDisjunction(const T &v) const {
                 const_iterator e = end();
                 for (const_iterator it = begin(); it != e; it++) {
                     const Literal &l = *it;
                     if (l.getPolarity()) {
                         if (v[l.getId()]) {
                             return true;
                         }
                     } else {
                         if (!v[l.getId()]) {
                             return true;
                         }
                     }
                 }
                 return false;
             }

         /**
          * Write the Clause to a stream.
          *
          * @return The input stream.
          */
         friend std::ostream& operator<<(std::ostream& os, const Clause &c) {
             os << '{';
             bool first = true;
             const_iterator e = c.end();

             for(const_iterator it = c.begin();
                     it != e;
                     it++) {
                 if(first)
                     first = false;
                 else
                     os << ", ";
                 os << *it;
             }
             os << '}';
             return os;
         }
    private:
         // the set that stores the literals
         hash_clauses_t literals;
         // the current max id
         size_t maxID;

};

} // namespace bfr

#endif  // CLAUSE_HPP_
